package net.greyar.theory;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

public class Substitution {
	private String string;
	private Map<Symbol, Symbol> bindings;
	private Map<Symbol, Set<Constraint>> constraints;
	private Set<Constraint> catalog;
	public Substitution() {
		bindings = new HashMap<Symbol, Symbol>();
		constraints = new HashMap<Symbol, Set<Constraint>>();
		catalog = new HashSet<Constraint>();
		toString(new StringBuilder());
	}
	@Override
	public String toString() {
		return string;
	}
	private StringBuilder toString(StringBuilder sb) {
		int start = sb.length();
		sb.append("{");
		int i = 0;
		for (Symbol variable : bindings.keySet()) {
			sb.append("[");
			variable.toString(sb);
			sb.append(" -> ");
			bindings.get(variable).toString(sb);
			sb.append("]");
			if (i != bindings.size() - 1) {
				sb.append(" ");
			}
			i++;
		}
		sb.append("}");
		sb.append(" ");
		sb.append("{");
		i = 0;
		for (Symbol variable : constraints.keySet()) {
			sb.append("[");
			variable.toString(sb);
			sb.append(" == ");
			int j = 0;
			for (Constraint constraint : constraints.get(variable)) {
				constraint.toString(sb);
				if (j != constraints.get(variable).size() - 1) {
					sb.append(", ");
				}
				j++;
			}
			sb.append("]");
			if (i != constraints.size() - 1) {
				sb.append(" ");
			}
			i++;
		}
		sb.append("}");
		string = sb.substring(start);
		return sb;
	}
	public Substitution bind(Symbol variable, Symbol symbol) {
		bindings.put(variable, symbol);
		toString(new StringBuilder());
		return this;
	}
	public boolean bound(Symbol variable) {
		return bindings.get(variable) != null;
	}
	public Symbol get(Symbol variable) {
		return bindings.get(variable);
	}
	public Symbol last(Symbol variable) {
		if (bound(variable)) {
			Symbol next = get(variable);
			while (next instanceof Variable && bound(next) && get(next) != variable) {
				next = get(next);
			}
			return next;
		}
		return variable;
	}
	public Substitution copy() {
		Substitution sigma = new Substitution();
		for (Symbol variable : bindings.keySet()) {
			sigma.bind(variable, bindings.get(variable));
		}
		for (Symbol variable : constraints.keySet()) {
			for (Constraint constraint : constraints.get(variable)) {
				sigma.addConstraint(variable, constraint);
			}
		}
		return sigma;
	}
	private Substitution addConstraint(Symbol variable, Constraint constraint) {
		catalog.add(constraint);
		if (!constraints.containsKey(variable)) {
			constraints.put(variable, new HashSet<Constraint>());
		}
		constraints.get(variable).add(constraint);
		toString(new StringBuilder());
		return this;
	}
	public Substitution constrain(Symbol one, Symbol other) {
		Constraint constraint = null;
		for (Constraint present : catalog) {
			if (one == present.getOne() && other == present.getTwo()
					|| other == present.getOne() && one == present.getTwo()) {
				constraint = present;
			}
		}
		if (constraint == null) {
			constraint = new Constraint(one, other);
			catalog.add(constraint);
		}
		for (Variable variable : one.getVariables()) {
			if (!constraints.containsKey(variable)) {
				constraints.put(variable, new HashSet<Constraint>());
			}
			constraints.get(variable).add(constraint);
		}
		for (Variable variable : other.getVariables()) {
			if (!constraints.containsKey(variable)) {
				constraints.put(variable, new HashSet<Constraint>());
			}
			constraints.get(variable).add(constraint);
		}
		toString(new StringBuilder());
		return this;
	}
	public boolean constrained(Symbol variable) {
		return constraints.containsKey(variable);
	}
	public Substitution satisfy(Symbol variable, Symbol value) {
		Substitution sigma = copy();
		sigma.bind(variable, value);
		Set<Constraint> constraints = this.constraints.get(variable);
		for (Constraint constraint : constraints) {
			sigma = constraint.satisfy(sigma);
			if (sigma == null) {
				return null;
			} else {
				if (value instanceof Variable) {
					sigma = sigma.addConstraint(value, constraint);
				}
			}
		}
		return sigma;
	}
}
